$\forall$${\it es}$:ES\{i\}, $e$:E, ${\it ds}$:$x$:Id fp$\rightarrow$ Type\{i\}, $P$:(State(${\it ds}$)$\rightarrow\mathbb{P}$\{i'\}), $j$:Id. $e$:$s$.$P$($s$)@$j$  $\in$ $\mathbb{P}$\{i'\}